\begin{tabbing}
weakPrecondSendR2\=\{\$a:ut2, \$tg:ut2\}\+
\\[0ex]($T$; $t$; $p$; $l$; ${\it ds}$; $P$; $f$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$([\=Rpre(source($l$);${\it ds}$;"\$a";$p$;$P$); \+
\\[0ex]
\\[0ex]Rsends(${\it ds}$;locl("\$a");p{-}outcome($p$);$l$;"\$tg" : $T$;[\=$<$"\$tg"\+
\\[0ex], $\lambda$$s$,$v$. [\=if $P$($s$)\+
\\[0ex]then $f$($s$,$v$)
\\[0ex]else $t$
\\[0ex]fi  / 
\\[0ex][]]
\-\\[0ex]$>$ / 
\\[0ex][]]) / 
\-\\[0ex][Rsframe($l$;"\$tg";[locl("\$a") / []]) / []]])
\-
\end{tabbing}